T:Type, f:(TT), x, y:T. x is f*(y)  ((x = y))  x is f*(f(y)) 

latex

Definitions	s = t, t  T, False, Type, x:AB(x), type List, a < b, x:A. B(x), , [car / cdr], last(L), P  Q, i  j , ||as||, x:A  B(x), P & Q, hd(l), y=f*(x) via L, True, x:A. B(x), y is f*(x), f(a), null(as), b, A, [], as @ bs, A List, i <z j, i z j, l[i], #$n, n - m, {i..j}, , {x:A| B(x)} , n+m, Void, A  B, t  ...$L, -n, , i  j < k, P  Q, P  Q, s ~ t, T
Lemmas	squash wf, iff wf, rev implies wf, select append front, assert wf, nat wf, member wf, le wf, length nil, length cons, non neg length, length append, length wf1, int seg wf, append wf, last wf, last lemma, fun-path wf, fun-connected wf, true wf, not wf, false wf